\documentclass[12pt]{beamer}


\usetheme{Pittsburgh} 

\usepackage[T2A]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage[english,russian]{babel} 
\usepackage{algorithmic}
\usepackage{algorithm}
\usepackage{graphicx}

\usepackage{multirow}


\setbeamertemplate{footline}{ \hfill \large{\insertframenumber / \inserttotalframenumber} \hspace*{.5cm}} 

\title{Применение технологии CUDA для решения задачи выполнимости булевых формул}
\author{вополнил: Курбацкий Евгений\\
научный руководитель: Бухановский Александр Валерьевич}
\date{\today}

\begin{document}

\frame{\titlepage}

\section{Вступление}
\subsection{Задача выполнимости}
\frame{
    \frametitle{Задача выполнимости}

 \begin{itemize}
 \item
	SAT --- самая известная NP-полная задача. Применяется:
    	\begin{itemize}
    	\item
        		в верификации
	\item
	            в схемотехнике
	\end{itemize}
 \item
	Алгоритм DPLL --- формирует базис для более эффективных, полных решателей SAT.
 \end{itemize}
}

\subsection{Алгоритм DPLL}
\frame
{
  \frametitle{Алгоритм DPLL}
    \begin{center}
        \includegraphics[width=110mm]{pics/DPLLtree.pdf}
   \end{center}
\begin{itemize}
    \item
	Основная идея в разбиении формулы на формулы меньшего размера. 
    \item
	Можно распаралелить
    \item
	Для распаралеливания можно использоват CUDA
\end{itemize}
}

\frame{
   \frametitle{Постановка задачи}  
   \begin{itemize}
   \item
       Реализовать различные варианты алгоритма DPLL
   \item
      Оптимизировать их при помощи технологии CUDA
   \item
      Оценить какой прирост дает применение CUDA
   \item
      Оценить эффективность алгоритмом в сравнении с существующими
   \end{itemize}
}

\frame{
   \frametitle{Проблемы}    

   \begin{itemize}
   \item
     CUDA является SIMD архитекрурой
   \item
     Дерево обхода DPLL может быть несбалансированным
   \item
     Операция персесылки данных между оперративной памятью и видеокартой занимает много времени
   \item
     Для получения хорошей производительности на CUDA требуется запускать тысячи  поторков
   \end{itemize}
}

\section{Реализация}

\frame{
    \frametitle{Проблема балансировки}
    \begin{columns}[c]
    \column{2.5in}
    Возникает проблема балансировки. Для решения данной проблемы алгоритм позволяет 
динамически распределять нагрузку между потоками.     
    \column{2in}
       \includegraphics[width=50mm]{pics/Forks.pdf}
    \end{columns}
}

\frame{
    \frametitle{Проблема пересылки данных}
Представим алгоритм в виде автомата. Реализуем каждое состояние в отдельном ядре.
    \begin{center}
    	\includegraphics[width=120mm]{pics/fsm.pdf}
    \end{center}
}

\frame{
    \frametitle{Балансировка анализа формулы}
    \begin{center}
    	\includegraphics[width=110mm]{pics/Balance.pdf}
    \end{center}
}

\subsection{Look-Ahead}
\frame{
    \frametitle{Look-Ahead}
    \begin{center}
    	\includegraphics[width=60mm]{pics/LookAheadTree.pdf}\\
    \end{center}
    \begin{itemize}
    \item
	Алгоритм look-ahead для каждой переменной формулы вычисляет весовую функцию.  \\
    \item
        Каждую из переменных можно обрабатывать независимо.
    \item
        Для того что бы полностью загрузить GPU требуется совместить с методом разделяй и властвуй.
    \end{itemize}
}

\section{Результаты}

\frame{
    \frametitle{Испробованные подходы}
    \begin{center}
	\includegraphics[width=110mm]{pics/Algorithms.pdf}
    \end{center}
}

\frame{  
    \frametitle{Эксперименты}
    \begin{itemize}
    \item
	Был проведен ряд экспериментов
    \item
	В качестве тестовых данных использовались тесты с соревнований sat решателей
    \item
	Каждый тест был ограничен по времени одной минутой
    \end{itemize}
}


\frame{
    Сравнение времени работы простого алгоритма DPLL на CPU и алгоритма DPLL на CUDA.\\
    \begin{center}
    	\includegraphics[width=85mm]{pics/SimpleVsCpu.pdf}\\
    \end{center}
 
}

\frame{  
   Сравнение времени работы алгоритма Look-Ahead на CPU и алгоритма Look-Ahead на CUDA.\\
    \begin{center}
	\includegraphics[width=85mm]{pics/LookAheadVsCpu.pdf}\\
    \end{center}
}

\frame{  
   Сравнение времени работы алгоритма с изучением новых дизъюнктов на CPU и  на CUDA.\\
    \begin{center}
	\includegraphics[width=85mm]{pics/LearnVsCpu.pdf}\\
    \end{center}
}


\frame{
    \begin{center}
	\includegraphics[width=90mm]{pics/Histogram.pdf}\\
    \end{center}
}

\frame{
    Сравнение времени работы алгоритма с изучением новых дизъюнктов и алгоритма Look-Ahead\\
    \begin{center}
	\includegraphics[width=90mm]{pics/LearnVsLookAhead.pdf}\\
    \end{center}
}

\frame{
    Сравнение времени работы Minisat и алгоритма Look-Ahead на CUDA.\\
    \begin{center}
	\includegraphics[width=90mm]{pics/LookAheadVsMiniSat.pdf}
    \end{center}
}

\frame{
    \frametitle{Результаты}
    \begin{center}
	\begin{tabular}{|l|l|l|l|}
	\hline
	\multirow{2}{*}{алгоритм} & cреднее & максимальное & тестов \\
	 & ускорение  & ускорение &  пройдено \\
	\hline
	DPLL & 2.6 & 9 & 231 / 433\\
	 Look-Ahead & 4.8 & 6 & 312 / 433 \\
	 Обучающийся & 3.2 & 7 & 286 / 433 \\
	 \hline
     	\end{tabular}
    \end{center}
}



\frame{
    \frametitle{Выводы}
    \begin{itemize}
    \item
    	Реализация алгоритма DPLL на CUDA допустима.
    \item
    	Реализация дает ускорение от 3 до 9 раз.
    \item
    	Реализация требует доработки:
        \begin{itemize}
            \item
                Совмещение с реализацией на CPU.
            \item
            	Добавления эвристик.
        \end{itemize}
    \end{itemize}
}

\frame{
\frametitle{Вопросы}
\begin{center}
	\Huge{Вопросы?}
\end{center}
}

\end{document}

